es:ES, L:(Id List).
fischer(L)
 (e1:E, j:Id.
 Try(e1)
  (j  L)
  ((j = loc(e1)))
  (sender(the rcv(wanted message from e1 to j)) = e1)) 

latex

Definitions	, P & Q, IdLnk, t  T, P  Q, P  Q, "$x", the rcv(wanted message from e1 to j), P  Q, Id, x:A. B(x), xL. P(x), A c B, Try(e), fischer(L)
Lemmas	event system wf, fischer wf, f-try wf, l member wf, es-loc wf, Id wf, not wf, es-sender-first-from, es-E wf